HOL Light
HOL 系の Theorem prover
by
John Harrison
HOL の最初のバージョンを作った Mike Gordon は John Harrison の先生
GitHub
https://github.com/jrh13/hol-light/
HOL Light ホームページ
https://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
HOL Light チュートリアル
https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf
HOL Light は OCaml の内部 DSL として書かれている
#Math
#数学基礎論
#Proof_assistant